es:ES, i:Id, e:E, P, R:({e:E| loc(e) = i }Prop).
(e:E. loc(e) = i  Dec(R(e)))
 (es-first-at-since(es;i;e;e.R(e);e.P(e))
 (
 (loc(e) = i
 (& P(e) & R(e)
 (& & ((e'':E. (e'' <loc e) & P(e''))
 (& & ( (e':E.
 (& & ( ((e' <loc e)
 (& & ( (& R(e') & (e'':E. (e' <loc e'')  (e'' <loc e)  P(e'') & R(e''))))) 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s), P  Q, A & B, P & Q, x:A. B(x), P  Q, t  T, x. t(x), e  e' , P  Q, es-first-at-since(es;i;e;e.R(e);e.P(e)), e<e'. P(e), A, (e <loc e'), False
Lemmas	es-E wf, es-locl wf, es-loc-pred, es-locl-iff, Id wf, es-loc wf, es-first-at-since wf, not wf, decidable wf, event system wf, previous-event-exists, es-le wf, es-le-loc, es-le-not-locl